Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar1/SK90SLASH2.61.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

F₂(j₂(x, y), y) -> G₁(f₂(x, k₁(y)))
F₂(j₂(x, y), y) -> K₁(y)
H2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> H2₃(s₁(x), y, h1₂(s₁(z), u))
F₂(x, h1₂(y, z)) -> H2₃(0, x, h1₂(y, z))
G₁(h2₃(x, y, h1₂(z, u))) -> H2₃(s₁(x), y, h1₂(z, u))
F₂(j₂(x, y), y) -> F₂(x, k₁(y))

The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F₂(j₂(x, y), y) -> G₁(f₂(x, k₁(y)))
F₂(j₂(x, y), y) -> K₁(y)
H2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> H2₃(s₁(x), y, h1₂(s₁(z), u))
F₂(x, h1₂(y, z)) -> H2₃(0, x, h1₂(y, z))
G₁(h2₃(x, y, h1₂(z, u))) -> H2₃(s₁(x), y, h1₂(z, u))
F₂(j₂(x, y), y) -> F₂(x, k₁(y))

The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 2 SCCs with 4 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPAfsSolverProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> H2₃(s₁(x), y, h1₂(s₁(z), u))

The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

H2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> H2₃(s₁(x), y, h1₂(s₁(z), u))

Used argument filtering: H2₃(x1, x2, x3) = x2
j₂(x1, x2) = j₁(x1)
Used ordering: Precedence:

trivial

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

F₂(j₂(x, y), y) -> F₂(x, k₁(y))

The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

F₂(j₂(x, y), y) -> F₂(x, k₁(y))

Used argument filtering: F₂(x1, x2) = x1
j₂(x1, x2) = j₁(x1)
k₁(x1) = k
h₁(x1) = h
h1₂(x1, x2) = h1
0 = 0
s₁(x1) = s
Used ordering: Precedence:

k > h1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPAfsSolverProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f₂(j₂(x, y), y) -> g₁(f₂(x, k₁(y)))
f₂(x, h1₂(y, z)) -> h2₃(0, x, h1₂(y, z))
g₁(h2₃(x, y, h1₂(z, u))) -> h2₃(s₁(x), y, h1₂(z, u))
h2₃(x, j₂(y, h1₂(z, u)), h1₂(z, u)) -> h2₃(s₁(x), y, h1₂(s₁(z), u))
i₁(f₂(x, h₁(y))) -> y
i₁(h2₃(s₁(x), y, h1₂(x, z))) -> z
k₁(h₁(x)) -> h1₂(0, x)
k₁(h1₂(x, y)) -> h1₂(s₁(x), y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.